/*
 *  SableJBDD, a Java Binary Decision Diagram package.
 *  Copyright (C) 2003  Feng Qian
 *
 *  This library is free software; you can redistribute it and/or
 *  modify it under the terms of the GNU Lesser General Public
 *  License as published by the Free Software Foundation; either
 *  version 2.1 of the License, or (at your option) any later version.
 *
 *  This library is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 *  Lesser General Public License for more details.
 *
 *  You should have received a copy of the GNU Lesser General Public
 *  License along with this library; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
//$Id: FiniteDomain.java,v 1.6 2004/03/15 02:07:20 fqian Exp $

package SableJBDD.fdd;

import SableJBDD.bdd.JBddManager;
import SableJBDD.bdd.JBddVariable;
import SableJBDD.bdd.JBDD;

import java.util.Map;
import java.util.HashMap;

import java.io.PrintStream;

/**
 * A finite domain provides constructions and operations of 
 * BDD functions on a finite set of variables.
 *
 * @author Feng Qian
 */
public class FiniteDomain {

  // DEBUG flag
  private static final boolean DEBUG = true;
  
  private JBddManager    bddm;            // underlying bdd manager
  private String         domainName;      // domain name
  private JBddVariable[] domainVariables; // domain variables
  private boolean enableAutoExpansion = false;
  
  /**
   * Defines a finite domain with a BDD manager, a domain name, and
   * the domain capacity.
   */
  public FiniteDomain(JBddManager manager, String name, int size) {
    // count bits 
    int numbits = countBitsOf(size - 1);
    int levels[] = new int[numbits];
    int toplevel = manager.getNumberOfVariables();

    for (int i=0; i<numbits; i++) {
      levels[i] = toplevel + numbits - i - 1;
    }

    initialize(manager, name, levels);
  }
 
  /**
   * Defines a finite domain with a BDD manager, a domain name, domain 
   * capacity, and a flag indicating whether the domain can be expanded
   * automatically.
   */
  public FiniteDomain(JBddManager manager, String name, int size, 
                      boolean expandible) {
    this(manager, name, size);
    this.enableAutoExpansion = expandible;
  }
  
  /**
   * Defines a finite domain with a bdd manager and variables at
   * specific levels.
   */
  public FiniteDomain(JBddManager manager, String name, int[] varidxes) {
    initialize(manager, name, varidxes); 
  }

  /**
   * Defines a finite domain with a bdd manager, name, variables at
   * specific levels, and a expandible flag.
   */ 
  // the order of variables, this also decides the initial 
  // capacity of the domain. least signaficant bit first
  // (zero index is the zero bit)
  public FiniteDomain(JBddManager manager, String name, int[] varidxes, boolean expandible) {
    this(manager, name, varidxes);
    this.enableAutoExpansion = expandible;
  }
  
  private void initialize(JBddManager manager, String name, int[] varidxes) {
    // assert (varidxes.length <= 32) : "domain lenth "+varidxes.length+" exceeds 32";  // support up to 0 ~ (2^31 - 1);
    
    this.bddm = manager;
    this.domainName = name;
    this.domainVariables = new JBddVariable[varidxes.length];
    for (int i=0, n=varidxes.length; i<n; i++) {
      this.domainVariables[i] = this.bddm.newVariableAtLevel(varidxes[i]);
      this.domainVariables[i].setName(name+i); 
    }

    if (DEBUG) System.out.println("domain "+name+" allows "+this.domainVariables.length+" variables");
  }

  /**
   * Gets a BDD function representing the ith element of this domain.
   * Side effect: if i exceeds the capacity of this domain, 
   * the domain is expanded automatically by allocating
   * new variables from the underlying BDD manager.
   * It is user's reponsibility to ensure the right order and
   * capacity of a domain.
   *
   * @param i an integer
   * @return the BDD function for ith element
   */
  public JBDD ith(int i) {
    int ibits = countBitsOf(i);

    if (ibits > this.domainVariables.length) { 
      if (this.enableAutoExpansion)   
        expandDomainVariables(i);
      // assert (!this.enableAutoExpansion): "value "+i+" exceeds domain capacity "+this.domainVariables.length;
    }
    
    // least significant bit first is necessary to extend the 
    // variables dynamically, the new varaible is appended to
    // the list which represents the high bit of the domain
    JBDD result = this.bddm.ONE();
    for (int j=0, n=this.domainVariables.length; j<n; j++) {
      if ( (i & (1 << j)) != 0) 
        result = result.and(this.bddm.posBddOf(this.domainVariables[j]));
      else 
        result = result.and(this.bddm.negBddOf(this.domainVariables[j]));
    }
    return result;
  }

  // returns the minimum number of bits to accomodate the value 
  private int countBitsOf(int x) {
    for (int p=31; p>=0; p--) {
      if ((x & (1 << p)) != 0) return p + 1;
    }
    return 0;
  }
  
  // check if n exceeds the domain capacity
  private synchronized void expandDomainVariables(int n) {
    int p = countBitsOf(n);
    // assert (p > this.domainVariables.length);

    JBddVariable[] newvars = new JBddVariable[p];
    System.arraycopy(this.domainVariables, 0,
                     newvars, 0, this.domainVariables.length);
    for (int i=this.domainVariables.length; i<p; i++) {
      newvars[i] = this.bddm.newVariable(this.domainName+i);
    }
    this.domainVariables = newvars;
  }
  
  /**
   * @return a BDD function representing the conjunction of variables 
   * in this domain.
   */
  public JBDD domainRepresentation() {
    JBDD rep = this.bddm.ONE();
    for (int i=0, n=this.domainVariables.length; i<n; i++) {
      rep = rep.and(this.bddm.posBddOf(this.domainVariables[i]));
    }
    return rep;
  }

  /**
   * Replaces domain variables in a BDD by variables in another domain.
   * Two domains must be compatible:
   * <ul>
   *  <li> the same bdd manager,
   *  <li> the same number of variables, and
   *  <li> BDD to be replaced must not contains variables of target domain.
   * </ul>
   *
   * @param x the bdd to be replace
   * @param other the target domain
   * @return the new BDD function after replacement
   */
  public JBDD replace(JBDD x, FiniteDomain other) {
    // assert (this.bddm == other.bddm);
    // assert (this.domainVariables.length == other.domainVariables.length);

    Map<JBddVariable,JBddVariable> map = new HashMap<JBddVariable,JBddVariable>();
    for (int i=0, n=this.domainVariables.length; i<n; i++) {
      map.put(this.domainVariables[i], other.domainVariables[i]);
    }

    return x.replace(map);
  }

  /**
   * Applies existential quantification on variables of this domain.
   * 
   * @param f the BDD function to be quantified
   * @return the resulted BDD function
   */
  public JBDD exist(JBDD f) {
    return f.exist(this.domainRepresentation());
  }

  /**
   * Reports variable orderings in this domain, from low to high.
   * 
   * @param out the print stream
   */
  public void reportOrdering(PrintStream out) {
    out.print(this.domainName+" : ");
    for (int i=0, n=this.domainVariables.length; i<n; i++) {
      out.print(this.domainVariables[i].getLevel()+" ");
    }
    out.println();
  }
}
